COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		Cartwright (1977) showed how to regard a LISP-type recursive
C00004 ENDMK
C⊗;
	Cartwright (1977) showed how to regard a LISP-type recursive
program as a sentence of first order logic.  Thus the well known
recursive definition of ⊗n! 

!!aa1:	%2n! ← qif n = 0 qthen 1 qelse n . (n - 1)!%1

gives rise to the sentence

!!aa2:	%2∀n.(n! = qif n = 0 qthen 1 qelse n . (n - 1)!%1.

	The formal similarity of ({eq aa1}) and ({eq aa2})
may be misleading; something substantial is being asserted.
({eq aa1}) is a computer program; it says that to compute the
value of ⊗n!,
one must evaluate the right hand side using the definition again
as necessary.  Such a rule defines a partial function, because there
is no guarantee that the evaluation process will terminate.  Indeed,
let us take the domain of ⊗n to be the set of all integers so that
the computation doesn't terminate for ⊗n negative.